COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	∂29-Jan-79  0941	CLT  
C00006 ENDMK
C⊗;
∂29-Jan-79  0941	CLT  
I will be glad to give you copies of whatever notes I use.  I plan to
talk about formal proofs of properties of LISP functions using FOL.
Remind me when you return.  I have a FOL version on the system containing
the language definitions and many proofs.  If you are interested, I'll
give you a brief demo sometime and you can play with it if you are interested.
When do I get a demo of your system?  I am in reading mode currently, so I'm
not at the lab too much, but my schedule is quite flexible so send me a note
when you are ready to demonstrate and I will appear.	---Carolyn---

∂02-Feb-79  0936	CLT  
xspool RWW[FOL,CLT] to get a copy of the notes for my talk to Richard's
class on Thursday.  In there is more there than I convered, as I had to
spend some time explaining LISP and didn't talk about the propositional
stuff.

∂07-Feb-79  1433	CLT  
Perhaps we could get together Monday morning.  I usually get here between
9 and 10.  The demo won't be particularly formal, but I can show you what 
is there, how to play with it, and maybe we can look at the theorem you
want to prove.

∂23-Feb-79  1027	CLT  
Unfortunately FOL has not learned about first order lambda expressions yet
(except to use to define function and pardicate parameter substitutions).
Thus and expression of the form:

f(x,a)=IF ATOM x THEN g(x) ELSE (λz.(IF NULL z THEN qNIL ELSE h(car z)) assoc(x,a))

must have the λ-converson done before giving it to FOL as in:

f(x,a)=IF ATOM x THEN g(x) ELSE IF NULL assoc(x,a) THEN qNIL ELSE h(car assoc(x,a))

If you are using λ's to avoid writing harry expressions more than once then
you can simulate this in FOL by making an extra definition whose righthand
side is the  harry expression and putting the definition in to relevant 
REWRITE simpsets.

In the next pass FOL will know about λ's, but for now you have to fake it.
I hope this answers your question.  If not, send me a particular example of a
definition you wish to make.

				---Carolyn---